package interfaces;

import tdg.contract.semanticAnnotations.ImportClass;
import tdg.contract.semanticAnnotations.Init;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Query;



@Init ({"getDescripcion()!=null"})
@Inv ({""})


public interface IProcedimientoDeMantenimiento {
	
	@Query
	public String getDescripcion();
	
	@Query
	public int getCodigoProcedimiento();
	
	@Pre({"nuevaDescripcion!=null #NullPointerException"})
	@Pos ({"getDescripcion().equals(nuevaDescripcion) && getCodigoProcedimiento()==getCodigoProcedimiento()@pre"})
	public void setDescripcion(String nuevaDescripcion);
	
	@Pre ({"nuevoCodigo>=0 && nuevoCodigo <= Integer.MAX_VALUE #IllegalArgumentException"})
	@Pos ({"getCodigoProcedimiento()== nuevoCodigo && getDescripcion().equals(getDescripcion()@pre)"})
	public void setCodigoProcedimiento(int nuevoCodigo);
}
